T:Type, eq:(TT). eq_seq(eq)  (k:  ({0..k}T))(k:  ({0..k}T)) 

latex

Definitions	ff, t  T, #$n, x:A. B(x), {i..j}, , a < b, A  B, x:A  B(x), P & Q, i  j < k, P  Q, False, A, {x:A| B(x)} , x:AB(x), f(a), p  q, x.A(x), tt, primrec(n;b;c), , , s = t, , b, b, P  Q, Unit, left + right, let x,y = A in B(x;y), Type, eq_seq(eq), (i = j)
Lemmas	nat wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bnot wf, not wf, assert wf, eq int wf, primrec wf, btrue wf, band wf, le wf, bool wf, int seg wf, bfalse wf